/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;

import org.eclipse.jdt.core.dom.AST;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.Modifier;
import org.eclipse.jdt.core.dom.QualifiedName;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.ThisExpression;
import org.eclipse.jdt.core.dom.InfixExpression.Operator;

import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.Fun;
import com.googlecode.syper.javasyp.formulae.Infix;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Name;
import com.googlecode.syper.javasyp.formulae.Prefix;
import com.googlecode.syper.javasyp.formulae.Quantifier;
import com.googlecode.syper.javasyp.formulae.Ref;

/**
 * @author kevin
 * @since May 30, 2010
 */
class HeapMapHavocLookup extends AbstractHavocLookup<HeapMapHavocLookup> {

	private final Map<ITypeBinding, Integer> heaps;

	public HeapMapHavocLookup(AST ast) {
		super(ast);
		heaps = new HashMap<ITypeBinding, Integer>();
	}

	private HeapMapHavocLookup(HeapMapHavocLookup original) {
		super(original);
		// heaps can be on different incarnations
		heaps = new HashMap<ITypeBinding, Integer>(original.heaps);
	}

	@Override
	public HeapMapHavocLookup createClone() {
		return new HeapMapHavocLookup(this);
	}

	/**
	 * Returns all fields
	 * @deprecated obsolete?
	 */
	@Deprecated
	@Override
	public Collection<Field> getKnownFields(Name n) {
		LinkedHashSet<Field> result = new LinkedHashSet<Field>();
		ITypeBinding clazz = n.getType();
		while (clazz != null) {
			for (IVariableBinding f : clazz.getDeclaredFields()) {
				if (! Modifier.isStatic(f.getModifiers()))
					result.add(getField(n, f));
			}
			clazz = clazz.getSuperclass();
		}
		return result;
	}

	@Override
	public Collection<Formula> havoc(Collection<Expression> es, boolean aroundLoop) {
		if (es.isEmpty())
			return Collections.emptySet();
		Map<ITypeBinding, Set<Field>> havoced =
			new LinkedHashMap<ITypeBinding, Set<Field>>();
		Set<ArrayAccess> arrays = new LinkedHashSet<ArrayAccess>();
		for (Expression e : es) {
			if (e instanceof ThisExpression)
				throw new IllegalArgumentException("Cannot havoc " + e);
			IVariableBinding binding;
			if (e instanceof SimpleName) {
				SimpleName var = (SimpleName) e;
				binding = (IVariableBinding) var.resolveBinding();
				if (binding.isEnumConstant()) {
					// do nothing
					continue;
				} else if (! binding.isField()) {
					// local (fields below)
					havocLocal(binding);
					continue;
				}
			} else if (e instanceof QualifiedName) {
				binding = (IVariableBinding) ((QualifiedName) e).resolveBinding();
			} else if (e instanceof FieldAccess) {
				binding = ((FieldAccess) e).resolveFieldBinding();
			} else if (e instanceof ArrayAccess) {
				arrays.add((ArrayAccess) e);
				continue;
			} else
				throw new IllegalArgumentException("Not an lvalue: " + e);

			Field f = (Field) getName(e);
			ITypeBinding heapType = getHeapType(e.resolveTypeBinding());
			Set<Field> fields = havoced.get(heapType);
			if (fields == null) {
				fields = new LinkedHashSet<Field>();
				havoced.put(heapType, fields);
			}
			fields.add(f);
		}

		Collection<Formula> result = havocHeapFields(havoced);
		if (! arrays.isEmpty()) {
			result = new LinkedHashSet<Formula>(result);
			for (ArrayAccess a : arrays) {
				result.addAll(havocArrayCell(a, aroundLoop));
			}
		}
		return result;
	}

	@Override
	public Collection<Formula> havoc(Map<Name, ? extends Collection<IVariableBinding>> modified) {
		if (modified.isEmpty())
			return Collections.emptySet();
		Map<ITypeBinding, Set<Field>> havoced =
			new LinkedHashMap<ITypeBinding, Set<Field>>();
		for (Entry<Name, ? extends Collection<IVariableBinding>> mod : modified.entrySet()) {
			final Collection<IVariableBinding> fs = mod.getValue();
			if (fs.isEmpty())
				continue;
			final Name access = mod.getKey();
			for (IVariableBinding field : fs) {
				if (field == null)
					throw new UnsupportedOperationException("array cell modification not supported");
				Field f = getField(access, field);
				ITypeBinding heapType = getHeapType(field.getType());
				Set<Field> fields = havoced.get(heapType);
				if (fields == null) {
					fields = new LinkedHashSet<Field>();
					havoced.put(heapType, fields);
				}
				fields.add(f);
			}
		}

		return havocHeapFields(havoced);
	}

	private Collection<Formula> havocHeapFields(
			Map<ITypeBinding, Set<Field>> havoced) {
		if (havoced.isEmpty())
			return Collections.emptyList();
		List<Formula> result = new ArrayList<Formula>(havoced.size());
		for (Map.Entry<ITypeBinding, Set<Field>> h : havoced.entrySet()) {
			ITypeBinding heapType = h.getKey();
			// havoc heap
			Integer incarnation = safeGet(heaps, heapType);
			incarnation = incarnation == null ? 0 : incarnation + 1;
			heaps.put(heapType, incarnation);
			if (incarnation == 0)
				// nothing to preserve...
				continue;

			// produce formula to preserve what's not havoced
			Set<Field> fields = h.getValue();
			Local objVar = new Local("o'", objType);
			Local fieldVar = Local.createFieldVar("f'", heapType);

			List<Formula> disjuncts = new ArrayList<Formula>(fields.size() + 1);
			for (Field f : fields) {
				disjuncts.add(Infix.toInfix(Operator.AND,
						Infix.equals(objVar, f.getObj()),
						Infix.equals(fieldVar, f.getSelector())));
			}
			disjuncts.add(Infix.equals(
					new Field(objVar, fieldVar, incarnation-1),
					new Field(objVar, fieldVar, incarnation)));
			result.add(Quantifier.forall(
					Arrays.asList(objVar, fieldVar),
					Infix.toInfix(Operator.OR, disjuncts)));
		}

		return result;
	}

	/**
	 * Havocs all heap cells except contents of the given references
	 * and final fields.
	 * This implementation havocs fields and array contents.
	 * Override this method to havoc additional parts of the heap.
	 * @param keep
	 * @param modifiable
	 * @return Formulae preserving information about {@code keepers}
	 */
	public Collection<Formula> havocHeap(Map<Name, PermKind[]> keep,
			Map<Name, ? extends Collection<IVariableBinding>> modifiable) {
		Collection<Formula> superResult = super.havocArrays(keep, modifiable);
		if (heaps.isEmpty())
			return superResult;

		List<Formula> result = new ArrayList<Formula>(heaps.size() + superResult.size());
		result.addAll(superResult);

		// havoc known heaps and preserve all fields other than n's
		for (Map.Entry<ITypeBinding, Integer> h : heaps.entrySet()) {
			int oldIncarnation = h.getValue();
			int newIncarnation = oldIncarnation + 1;
			h.setValue(newIncarnation);

			if (keep.isEmpty())
				// havoc entire heap
				continue;

			ITypeBinding heapType = h.getKey();
			Local objVar = new Local("o'", objType);
			Local fieldVar = Local.createFieldVar("f'", heapType);

			Set<Formula> toKeep = keepPredicate(objVar, keep, modifiable.keySet());
			// protect all final fields FIXME make this sound in constructor calls
			toKeep.add(Fun.pred(Fun.FINAL_PRED, fieldVar));

			result.add(Quantifier.forall(
					Arrays.asList(objVar, fieldVar),
					Infix.toInfix(Operator.OR,
							Prefix.not(Infix.toInfix(Operator.OR, toKeep)),
							Infix.equals(
									new Field(objVar, fieldVar, oldIncarnation),
									new Field(objVar, fieldVar, newIncarnation)))));
		}
		return result;
	}

	@Override
	protected String getProtectionPredicate(ITypeBinding heap) {
		if (!objType.equals(heap))
			return null;
		Integer inc = safeGet(heaps, heap);
		if (inc != null)
			return Fun.PROTECT_PRED + inc;
		else
			return null;
	}

	@Override
	public Field getField(Ref accessor, IVariableBinding field) {
		// normalize accessor
		if (accessor == null) {
			// FIXME resolution for inner classes
			accessor = new Local("this", field.getDeclaringClass());
		}

		ITypeBinding heapType = field == null ? intType : getHeapType(field.getType());
		Integer incarnation = safeGet(heaps, heapType);
		if (incarnation == null) {
			incarnation = 0;
			heaps.put(heapType, incarnation);
		}
		// TODO unify (currently need binding for "real" fields)
		if (field == null)
			return new Field(accessor,
					Local.createFieldVar(Local.ARRAY_LENGTH_FIELD_NAME, intType),
					incarnation);
		else
			// use normalized field binding
			return new Field(accessor, incarnation, field.getVariableDeclaration());
	}

	@Override
	protected void mergeLookups(Set<Formula> knowledge, HeapMapHavocLookup other) {
		super.mergeLookups(knowledge, other);

		for (Map.Entry<ITypeBinding, Integer> h1 : this.heaps.entrySet()) {
			ITypeBinding heapType = h1.getKey();
			Integer inc1 = h1.getValue();
			Integer inc2 = safeGet(other.heaps, heapType);
			if (inc2 != null) {
				if (inc1 < inc2) {
					Local objVar = new Local("o'", objType);
					Local fieldVar = Local.createFieldVar("f'", heapType);
					knowledge.add(Quantifier.forall(
							Arrays.asList(objVar, fieldVar),
							Infix.equals(
									new Field(objVar, fieldVar, inc1),
									new Field(objVar, fieldVar, inc2))));
					h1.setValue(inc2);
				} // else nothing to do here (symmetric merge will fix other
			} else {
				// force our incarnation onto the other heap
				other.heaps.put(heapType, inc1);
			}
		}
	}
}
